qadd_grp  abgrp{i:l} 

latex

Definitions	t.2, t.1, grp_op(g), grp_car(g), comm(T; op), inverse(T; op; id; inv), ident(T; op; id), assoc(T; op), P  Q, x. t(x), P  Q, prop{i:l}, P  Q, x f y, P  Q, x:A. B(x), eqfun_p(T; eq), qadd_grp, abgrp{i:l}, t  T, x(s), mon{i:l}, grp{i:l}, subtype(S; T)
Lemmas	qadd minus, qadd ident, qadd com, qadd assoc, assert-qeq, iff functionality wrt iff, assert wf, iff wf, all functionality wrt iff, qmul wf, int inc rationals, qadd wf, q le wf, qeq wf2, rationals wf, mk grp, grp op wf, grp car wf, comm wf